(g,p,q,E,z.  p  i < q. E(i))  g:IMonoidp,q:({p..q}|g|)(True)|g| 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	t  T, , x:A. B(x), T, IMonoid
Lemmas	imon wf, grp car wf, int seg wf, true wf, squash wf, mon itop wf